$\forall$$i$, $a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it init}$:$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Void, $P$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]@$i$ (with ds: ${\it ds}$ init: ${\it init}$ action $a$:$T$ precondition $a$(v) is $P$ s v) $\in$ Dsys